COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	FORMAL REASONING
C00015 ENDMK
C⊗;
FORMAL REASONING

The Formal Reasoning Project is making computers check human reasoning
in mathematics, computer science and common sense.  This is done
with a program called FOL that lets a user enter his reasoning in a modified
version of first order mathematical logic.  Since computers have been
generating proofs for years, we had better explain why we are doing
something as apparently dull as merely checking them.

While some interesting results have been obtained by computer theorem
provers, and Dave Luckham in this Laboratory has even found some results
of mathematical interest before they were proved by any human, computer
theorem provers are still a long way from human reasoning power.  The
difficulties come from two sources.  The best understood source of
difficulty is called the combinatorial explosion.  At each stage in
the reasoning there are many possibilities for drawing conclusions
from the previous results, and sometimes many steps have to be generated
before it is clear whether progress is being made or another false trail
is being followed.  The more steps of reasoning the eventual proof is
going to have, the more likely it is that the prover will be defeated
by the combinatorial explosion.

Besides these so-called heuristic difficulties, there are also what are
called epistemological difficulties in deciding precisely what knowledge
is basic to the problem, how to express that knowledge in the memory
of the computer, and what methods of reasoning to allow.  A proof-checker
allows us to verify our understanding of these matters, and the preliminary
results show that artificial intelligence has a long way to go in
understanding the epistemology of mathematics, of computer science, and
above all, of common sense reasoning.
Once the formalism exists for expressing human reasoning in a satisfactory
way, it will be much less mysterious how to make computer programs generate
it.  Incidentally, computer theorem proving is important not merely for
itself, but because there exist well known techniques for going from a formal
proof that a solution exists to a problem to the solution itself.

The best understood area is pure mathematics.  Computer checkable proofs
of mathematical theorems of medium difficulty are about ten times as
long as the informal proofs in the mathematics textbooks, and FOL
proof-checker allows much briefer proofs than the those the theorem
proving programs can generate.  This might not be so bad in itself, but
the combinatorial explosion difficulty is made much worse when very long
proofs have to be generated.

The next area is proofs of the correctness of computer programs, and this
has applications apart from artificial intelligence.  Namely, computer
checkable proofs that a computer program or a piece of hardware meets
its specifications constitute the most promising tool for getting out
of the long debugging cycles of the large systems used in defense and
in industry.

The third area is common sense reasoning where even the basic facts on
which human reasoning is based remain to be discovered.

The Formal Reasoning Group at the Stanford Artificial Laboratory is
pursuing a systematic program for making computer checked proofs a
useful tool in themselves and using them to advance artificial intelligence.
Here are some recent results:

	The first group of results is the proof of several theorems in
mathematics.  Each problem is beyond the capacity of present computer
theorem provers, and each exhibits a different aspect of reasoning.
Each proof is being carefully examined to see how its length can be
reduced to the length of a mathematician's informal proof by adding
new methods of reasoning.

	The easiest of theorems proved is that a prime number divides
a product only if it divides one of the factors.  In the standard
development of mathematics, it is about the first theorem that is
not proved by mathematical induction - which is about the most
advanced tool used by automatic theorem provers.  Making its proof
short requires organizing a substantial body of arithmetic facts
and making them available to the proof checker.

	A more difficult result along similar lines is Wilson's theorem.
"If p is a prime number it divides (p-1)!+1.  Thus 5 divides 4!+1 = 25, and 7
divides 6!+1 = 721.  The proof is not at all obvious and requires
arranging the numbers between 1 and p-1 in pairs such that the product of
each pair has remainder 1 when divided by p.  Tying down the description
of this pairing requires the ability to handle sets neatly, and the
length of the proof shows that set theory has to be reformulated in
a way that expresses informal arguments better.  Many ideas for doing
this are suggested by the experience.

	A proof of correctness of a binary ripple-carry adder was a
first step towards proving the correctness of computer hardware.  This
one was quite easy an suggests that a harder hardware problem be
undertaken.

	The most difficult mathematical result was Ramsey's theorem
that if an infinite number of points are connected pairwise with
red and black threads, there is either an infinite subset entirely
connected by red threads or an infinite set entirely connected by
black threads.  The difficulties are in treating infinite sets properly
and in representing the rather peculiar mathematical induction argument
used in the proof.

	While mathematics provides the most accessible examples of precise
human reasoning that can be checked, it is all syllogistic, and based on
axioms expressed in a way that experience has shown suitable for
mathematics.  However, much
informal human reasoning combines observation with syllogistic reasoning.
and it is not so obvious how the facts on which the reasoning is based
are to be expressed.  A chess puzzle provided an example wherein the
facts were precise enough but had to be expressed in a quite different
way than in mathematical problems and where the reasoning involved a
mixture of observation using a program called the "chess-eye" and the
more familiar syllogistic reasoning.

	Common sense reasoning requires a study of the basic facts of
common sense.  McCarthy has been working for some time on basic facts
about people's knowledge and the location of information.  This includes,
for example, how to express what a traveller knows about who knows
airplane schedules and where telephone numbers are to be found
and the fact that it is not necessary to know the gate of an airplane
leaving an intermediate stop in a trip, because the information will
be available when needed.  In conjunction with researchers from
Kyoto University in Japan, McCarthy developed a set of axioms for
expressing what people know about what other people know.  This
system is adequate for expressing the facts of a well-known puzzle
involving three wise men asked to guess the color of spots painted
on their foreheads.  In this research, it came out that the problem
of concluding that someone will not know something is much deeper than
the problem of concluding that he will know it and requires entirely
new mathematical methods.

	Work in the mathematical theory of computation continued with
the further development by McCarthy of his theory of extensional forms
aimed at combining the power of methods of reasoning about programs
developed by Dana Scott at Oxford with the power of set theory in
first order logic.

	It is the opinion of the Stanford Artificial Intelligence
Laboratory that the study of formal reasoning is fundamental to further
progress in artificial intelligence.